/*******************************************************************\

Module: Main Module 

Author: Daniel Kroening, kroening@kroening.com

\*******************************************************************/

/*

  WOLVERINE
  Interpolation for ANSI-C
  Copyright (C) 2008
  Daniel Kroening <kroening@kroening.com>
  Georg Weissenbacher <georg@weissenbacher.name>

*/
#ifndef TESTMAIN_H
#define TESTMAIN_H
#include <config.h>
#include <cmdline.h>
#include <ui_message.h>
#include <options.h>

#include <goto-programs/goto_functions.h>
#include <goto-programs/goto_convert_functions.h>

#include <langapi/language_ui.h>
#include <langapi/mode.h>
#include <ansi-c/ansi_c_language.h>

#ifdef HAVE_CPP
#include <cpp/cpp_language.h>
#endif

#include <cfa/cfa.h>
#include <cfa/typedef.h>

//#include "wolver_parseoptions.h"
//#include "path_interpolator.h"
#include <stdio.h>


extern string Expr2String(Expr* e);
//
int quake_test;//quake test
std::map<std::string, std::map<std::string, std::string> > struct_info;
std::map<std::string, std::map<std::string, int> > enum_info;
//extern ansi_c_parsert ansi_c_parser;

class tester_maint : public parseoptions_baset, language_uit {
public:
        tester_maint(int argc, const char **argv)
                : parseoptions_baset("", argc, argv),
                  language_uit("parse_test", cmdline) {}
        goto_functionst goto_functions;
        int doit() {
            vector<CFA> vnewCFA;
            return doit(vnewCFA);
        }
        int doit(vector<CFA> &vnewCFA) {
          register_language(new_ansi_c_language);
          #ifdef HAVE_CPP
          register_language(new_cpp_language);
          #endif
          if(config.set(cmdline)) {
                  error("Urgs");
                  exit(1);
          }
          if(get_goto_program(goto_functions, vnewCFA))
            return 6;
          return 0;
        }
private:
        bool get_goto_program(goto_functionst &goto_functions, vector<CFA> &vnewCFA) {
                try {
                        if(cmdline.args.size()==0) {
                                error("Nothing to do");
                            return true;
                        }
                        quake_test = 0; // quake test
                        if(parse()) return true;
                        if(typecheck()) return true;  //question 
                        if(final()) return true;      //        重複
                        //Get_Parse_Tree();//發現要如此宣告必須有一個繼承關係，不然不能用
                        // we no longer need any parse trees or language files
                        clear_parse();

                        // show symbol table: print content of symbol tabel
                        //show_symbol_table();

                        //status("Generating GOTO Program");

                        // context, options, dest
                        goto_convert(context, optionst(), goto_functions, ui_message_handler);
                        std::map<std::string, std::map<std::string, std::string> > s = struct_info;
                        if(process_goto_program(goto_functions, vnewCFA))
                                return true;
                }
                catch (const char *e) {
                        error(e);
                        return true;
                }
                catch (const std::string e) {
                        error(e);
                        return true;
                }
                catch (int) {
                      return true;
                }

                catch (std::bad_alloc) {
                        error("Out of memory");
                        return true;
                }
                return false;
        }
        bool process_goto_program(goto_functionst &goto_functions, vector<CFA> &vnewCFA) {
            namespacet ns(context);
                goto_functions.output(vnewCFA, ns, std::cout);
                //goto_functions.outputCFA(ns, std::cout);
                return false;
        }
};
#endif
//

/*******************************************************************\

Function: main

  Inputs:

 Outputs:

 Purpose:

\*******************************************************************/

/*int main(int argc, const char **argv)
{
  //wolver_parseoptionst parseoptions(argc, argv);
  // tester
  vector<CFA> vnewCFA;
  tester_maint tester_main (argc, argv);
  tester_main.doit(vnewCFA);
  vnewCFA.erase(vnewCFA.begin(), vnewCFA.begin()+2);
  cout << "========== Print CFA ============= " << endl;
  for(int i1 = 0; i1 < (int)vnewCFA.size(); i1++){
      cout << "CFA Name " <<  vnewCFA[i1].GetId() << endl;
      for(int i2 = 0; i2 < (int)(vnewCFA[i1].GetFormPara()).size(); i2++){
          cout << " === " << i1 << " ===formal " << Expr2String((vnewCFA[i1].GetFormPara())[i2])<< endl;
      }
      vnewCFA[i1].PrintCFA();
      string filename = vnewCFA[i1].GetId();
      filename = filename + ".dot";
      vnewCFA[i1].CFA2Dot(filename.c_str());
  }
  //return parseoptions.main();
  return 0;
}*/
